#pragma once

/**********************************************************
oxsat - portable sat solver for windows and unix
Copyright (C) 2017  tj bandrowsky

This program is free software; you can redistribute it and/or
modify it under the terms of the GNU General Public License
as published by the Free Software Foundation; either version 2
of the License, or (at your option) any later version.

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301, USA.
*/

#include "variable.h"
#include "production.h"
#include <list>
#include <vector>

namespace solver
{
	class problem_variable
	{
	public:
		variable_reference	ref;
		variable_name		name;
		int					value;
		bool				check_valid;
		int					values_used_mask;
		int					explicit_value;
		std::list<pproduction> productions;
	};

	class variable_manager 
	{
	public:
		std::vector<problem_variable> variables;

		std::string to_string(solver::production *cur_prod)
		{
			std::string implication_text = "";

			if (cur_prod->product.ref == -1)
			{
				implication_text = "Conflict <- ";
			}
			else
			{
				auto& v = variables[cur_prod->product.ref];
				if (cur_prod->product.val == 0)
				{
					implication_text += "!";
				}
				implication_text += std::to_string(v.name);
				implication_text += " <- ";
			}

			implication_text += to_string(cur_prod->match, " ");

			return implication_text;
		}

		std::string to_string(solver::pdecision dec)
		{
			std::string text;

			text = "(";
			bool written = false;
			size_t ds = dec->literals.size();
			for (int i = 0; i < ds; i++)
			{
				auto& vs = dec->literals[i];

				if (written) {
					text += " | ";
				}
				auto& v = variables[vs.ref];

				if (vs.val == 0) {
					text += "!";
					text += std::to_string(v.name);
				}
				else
				{
					text += std::to_string(v.name);
				}
				written = true;
			}
			text += ") at line ";
			text += std::to_string(dec->line_number);

			return text;
		}

		std::string to_string(solver::decision_string& dstr, const char *delimiter = nullptr)
		{
			std::string x = "";
			if (dstr.is_c_str) {
				auto dcdestn = dstr.first();
				while (dcdestn != nullptr)
				{
					auto& dcdest = dcdestn->value;
					if (!dcdest.val)
					{
						x += "!";
					}
					std::string temp(1, (char)variables[dcdest.ref].name);
					x += temp;
					if (delimiter != nullptr) {
						x += delimiter;
					}
					dcdestn = dstr.next(dcdestn);
				}
			}
			else {
				auto dcdestn = dstr.first();
				while (dcdestn != nullptr)
				{
					auto& dcdest = dcdestn->value;
					if (!dcdest.val)
					{
						x += "!";
					}

					x += std::to_string(variables[dcdest.ref].name);
					if (delimiter != nullptr) {
						x += delimiter;
					}
					dcdestn = dstr.next(dcdestn);
				}
			}
			return x;
		}
	};
}
